FDL - Nuprl Lemma : es-real-and

Nuprl Lemma : es-real-and_wf

0,22

P, Q:(ES{i}

Prop{i'}), X:es-real{i:l}(es.P(es)), Y:es-real{i:l}(es.Q(es)),

p:R-compat{i:l}

p:R-compat(1of(X); 1of(Y)).
es-real-and{i:l}(P; Q; X; Y; p)

es-real{i:l}(es.(P(es) & Q(es)))

Definitions x:A. B(x), Prop, es.P(es), x(s), 1of(t), t T, P & Q, es-real-and{i:l}(P;Q;X;Y;p), x:A. B(x), 2of(t), P Q, x. t(x)

Lemmas es realizer wf, R-realizes wf, R-compat wf, Rplus wf, es-real wf, event system wf

Definitions	x:A. B(x), Prop, es.P(es), x(s), 1of(t), t T, P & Q, es-real-and{i:l}(P;Q;X;Y;p), x:A. B(x), 2of(t), P Q, x. t(x)
Lemmas	es realizer wf, R-realizes wf, R-compat wf, Rplus wf, es-real wf, event system wf